home *** CD-ROM | disk | FTP | other *** search
/ Sprite 1984 - 1993 / Sprite 1984 - 1993.iso / lib / tex / vdm.sty < prev    next >
Text File  |  1988-04-18  |  21KB  |  520 lines
  1. \def\@fmtname{lplain}% FONT-CUSTOMIZING
  2. \newfam\amssyfam    % the Y series of AMS fonts
  3. \iffalse        % change to \ifx\fmtname\@fmtname if you have them
  4.     \gdef\amssy{\protect\pamssy} % \amssy will change font just like \bf
  5.     \def\@addto#1#2{\ifx#1\undefined % do nothing
  6.                 \else    \toks0=\expandafter{#1}\toks1={#2}%
  7.                 \global\edef#1{\the\toks0 \the\toks1 }\fi}
  8.     \@addto\vpt{\def\pamssy{\@getfont\pamssy\amssyfam\@vpt{msym5}}}
  9.     \@addto\vpt{\def\pamssy{\@getfont\pamssy\amssyfam\@vpt{msym5}}}
  10.     \@addto\vipt{\def\pamssy{\@getfont\pamssy\amssyfam\@vipt{msym6}}}
  11.     \@addto\viipt{\def\pamssy{\@getfont\pamssy\amssyfam\@viipt{msym7}}}
  12.     \@addto\viiipt{\def\pamssy{\@getfont\pamssy\amssyfam\@viiipt{msym8}}}
  13.     \@addto\ixpt{\def\pamssy{\@getfont\pamssy\amssyfam\@ixpt{msym9}}}
  14.     \@addto\xpt{\def\pamssy{\@getfont\pamssy\amssyfam\@xpt{msym10}}}
  15.     \@addto\xipt{\def\pamssy{\@getfont\pamssy\amssyfam\@xipt{msym10\@halfmag}}}
  16.     \@addto\xiipt{\def\pamssy
  17.         {\@getfont\pamssy\amssyfam\@xiipt{msym10\@magscale1}}}
  18.     \@addto\xivpt{\def\pamssy
  19.         {\@getfont\pamssy\amssyfam\@xivpt{msym10\@magscale2}}}
  20.     \@addto\xviipt{\def\pamssy
  21.         {\@getfont\pamssy\amssyfam\@xviipt{msym10\@magscale3}}}
  22.     \@addto\xxpt{\def\pamssy{\@getfont\pamssy\amssyfam\@xxpt{msym10\@magscale4}}}
  23.     \@addto\xxvpt{\def\pamssy
  24.         {\@getfont\pamssy\amssyfam\@xxvpt{msym10\@magscale5}}}
  25. \else
  26.     \global\let\amssy=\bf
  27. \fi
  28. \newenvironment{vdm}{\@beginvdm}{\@endvdm}
  29. \def\@beginvdm{\@changeMathmodeCatcodes}
  30. \def\@endvdm{\global\everypar={{\setbox0=\lastbox}%
  31.             \global\everypar={}%
  32.             \global\let\par=\@@par}
  33.     \global\let\par=\@undonoindent}
  34. \def\@undonoindent{\global\everypar={}\global\let\par=\@@par\@@par}
  35. \def\@beginVerticalVDM{\@changeLeftMargin\@changeBaselineskip}
  36. \newcount\@mathFamily  \@mathFamily=\itfam
  37. \everymath=\expandafter{\the\everymath\fam\@mathFamily
  38.     \@changeMathmodeCatcodes}
  39. \everydisplay=\expandafter{\the\everydisplay\fam\@mathFamily
  40.     \@changeMathmodeCatcodes}
  41. \mathcode`\0="0030
  42. \mathcode`\1="0031
  43. \mathcode`\2="0032
  44. \mathcode`\3="0033
  45. \mathcode`\4="0034
  46. \mathcode`\5="0035
  47. \mathcode`\6="0036
  48. \mathcode`\7="0037
  49. \mathcode`\8="0038
  50. \mathcode`\9="0039
  51. \def\defaultMathcodes{\@mathFamily=-1}
  52. \def\@changeOtherMathcodes{%
  53.     \mathcode`\:="603A
  54.     \mathcode`\-="042D
  55.     \mathcode`\|="326A
  56.     \mathchardef\Or="325F % this is a rel to get 5mu spacing
  57. }
  58. \def\@VDMunderscore{\leavevmode\kern.06em
  59.     \vbox{\hrule height.2ex width.3em}\hskip0.1em}
  60. {\catcode`\_=\active \catcode`\"=\active
  61. \gdef\@changeGlobalCatcodes{% make _ a normal char
  62.     \catcode`\_=\active \let_=\@VDMunderscore}
  63. \gdef\@changeMathmodeCatcodes{% make ~ mean \hook, " do text, @ mean subscript
  64.     \let~=\hook
  65.     \catcode`\@=8
  66.     \catcode`\"=\active  \let"=\@mathText}
  67. \gdef\underscoreoff{% make _ a normal char
  68.     \catcode`\_=\active \let_=\@VDMunderscore}
  69. \gdef\underscoreon{% restore underscore to usual meaning
  70.     \catcode`\_=8}
  71. \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
  72. \def\mathTextFont{\rm}
  73. \newdimen\VDMindent \VDMindent=\parindent
  74. \def\VDMbaselineskip{\baselineskip}
  75. \def\@changeLeftMargin{\leftskip=\VDMindent}
  76. \def\@changeBaselineskip{\baselineskip=\VDMbaselineskip}
  77. \ifx\fmtname\@fmtname
  78.     \def\keywordFontBeginSequence{\small\sf}%    user-definable
  79. \else
  80.     \def\keywordFontBeginSequence{\bf}%    good for SliTeX
  81. \fi
  82. \def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}
  83. \def\makeNewKeyword#1#2{%
  84.     \newcommand{#1}{\hbox{\keywordFontBeginSequence #2\/}}}
  85. \makeNewKeyword{\nil}{nil}
  86. \makeNewKeyword{\True}{true}
  87. \makeNewKeyword{\true}{true}
  88. \makeNewKeyword{\False}{false}
  89. \makeNewKeyword{\false}{false}
  90. \def\where{\par\moveright\VDMindent\hbox{\keywordFontBeginSequence where\/}}
  91. \def\newMonadicOperator#1#2{\newcommand{#1}{\kw{#2\kern.16667em}\nobreak}}
  92. \def\Bool{\hbox{\amssy B\/}}
  93. \def\Nat{\hbox{\amssy N\/}}
  94. \def\Nati{\hbox{$\hbox{\amssy N}_1$}}
  95. \let\Natone=\Nati % just for an alternative
  96. \def\Int{\hbox{\amssy Z\/}}
  97. \def\Real{\hbox{\amssy R\/}}
  98. \def\Rat{\hbox{\amssy Q\/}}
  99. \newenvironment{op}{\@beginVDMoperation}{\@endVDMoperation}
  100. \newenvironment{vdmop}{\@beginvdm\@beginVDMoperation}%
  101.     {\@endVDMoperation\@endvdm}
  102. \newbox\@operationNameBox
  103. \newif\ifArgumentListEncountered@
  104. \newtoks\@argumentListTokens
  105. \newtoks\@resultNameAndTypeTokens
  106. \newbox\@externalsBox
  107. \newbox\@preConditionBox
  108. \newbox\@postConditionBox
  109. \def\@beginVDMoperation{% clear temporaries, deal with optional arg
  110.     \setbox\@operationNameBox=\hbox{}
  111.     \@argumentListTokens={} \ArgumentListEncountered@false
  112.     \@resultNameAndTypeTokens={}
  113.     \setbox\@externalsBox=\box\voidb@x
  114.     \setbox\@preConditionBox=\box\voidb@x
  115.     \setbox\@postConditionBox=\box\voidb@x
  116.     \vskip\preOperationSkip
  117.     \@beginVerticalVDM
  118.     \bgroup
  119.     \advance\hsize by-\leftskip \leftskip=0pt %for inner constructions
  120.     \preOperationHook
  121.     \@ifnextchar [{\@opname}{}}
  122. \newcount\preOperationPenalty \preOperationPenalty=0
  123. \newcount\preExternalPenalty \preExternalPenalty=2000
  124. \newcount\prePreConditionPenalty \prePreConditionPenalty=800
  125. \newcount\prePostConditionPenalty \prePostConditionPenalty=500
  126. \newcount\postOperationPenalty \postOperationPenalty=-500
  127. \newskip\preOperationSkip \preOperationSkip=2ex plus 0.5ex minus 0.2ex
  128. \newskip\postOperationSkip \postOperationSkip=2ex plus 0.5ex minus 0.2ex
  129. \newskip\postHeaderSkip \postHeaderSkip=.5ex plus .2ex minus .2ex
  130. \newskip\postExternalsSkip \postExternalsSkip=.5ex plus .2ex minus .2ex
  131. \newskip\postPreConditionSkip \postPreConditionSkip=.5ex plus .2ex minus .2ex
  132. \def\@endVDMoperation{% make up operation
  133.     \@setOperationHeader
  134.     \egroup % matches the \bgroup in \@beginVDMoperation
  135.     \vskip\postHeaderSkip
  136.     \betweenHeaderAndExternalsHook
  137.     \ifvoid\@externalsBox
  138.     \else \moveright\VDMindent\box\@externalsBox
  139.           \vskip\postExternalsSkip
  140.     \fi
  141.     \betweenExternalsAndPreConditionHook
  142.     \ifvoid\@preConditionBox
  143.     \else \moveright\VDMindent\box\@preConditionBox
  144.           \vskip\postPreConditionSkip
  145.     \fi
  146.     \betweenPreAndPostConditionHook
  147.     \ifvoid\@postConditionBox
  148.     \else \moveright\VDMindent\box\@postConditionBox
  149.           \vskip\postOperationSkip
  150.     \fi
  151.     \postOperationHook}
  152. \def\preOperationHook{\penalty\preOperationPenalty }
  153. \def\betweenHeaderAndExternalsHook{\penalty\preExternalPenalty }
  154. \def\betweenExternalsAndPreConditionHook{\penalty\prePreConditionPenalty }
  155. \def\betweenPreAndPostConditionHook{\penalty\prePostConditionPenalty }
  156. \def\postOperationHook{\penalty\postOperationPenalty }
  157. \def\@setOperationHeader{%
  158.     \ifArgumentListEncountered@
  159.         \setbox\@operationNameBox=
  160.             \hbox{\unhbox\@operationNameBox\ (}\fi
  161.     \dimen255=\hsize \advance\dimen255 by-\wd\@operationNameBox
  162.      \noindent\kern-.05em\box\@operationNameBox
  163.     \vtop{\@raggedRight \hsize=\dimen255 \noindent
  164.         $\ifArgumentListEncountered@\the\@argumentListTokens)\fi
  165.         \ \the\@resultNameAndTypeTokens$}}
  166. \def\opname#1{\@opname[#1]}
  167. \def\@opname[#1]{\setbox\@operationNameBox=\hbox{$\relax#1$\ }}
  168. \def\args{\ArgumentListEncountered@true\@argumentListTokens=}
  169. \def\res{\@resultNameAndTypeTokens=}
  170. \newenvironment{externals}{\@beginExternals}{\@endExternals}
  171. \def\ext{\bgroup\@makeColonActive\@ext}
  172. \def\@ext#1{\@beginExternals#1\@endExternals\egroup}
  173. \def\@beginExternals{\global\setbox\@externalsBox=%
  174.     \@beginIndentedPara{\hsize}{ext }{\@setUpExternals}}
  175. \def\@endExternals{\@endIndentedPara{\@endAlignment}}
  176. \def\@setUpExternals{\@makeColonActive
  177.     \@changeLineSeparator\@beginAlignment}
  178. {\catcode`\:=\active
  179.  \gdef\@makeColonActive{\catcode`\:=\active \let:=&}}
  180. \def\@changeLineSeparator{\let\\=\cr} % for usr within \halign
  181. \def\@beginAlignment{\expandafter\halign\expandafter\bgroup
  182.     \the\@extAlign\strut\enspace&:\enspace$##$\hfil\cr}
  183. \def\@endAlignment{\crcr\egroup}
  184. \newtoks\@extAlign
  185. \def\leftExternals{\@extAlign={$##$\hfil}}
  186. \def\rightExternals{\@extAlign={\hfil$##$}}
  187. \leftExternals
  188. \makeNewKeyword{\Rd}{rd } \makeNewKeyword{\Wr}{wr }
  189. \newenvironment{precond}{\@beginPre}{\@endPre}
  190. \def\pre#1{\@beginPre#1\@endPre}
  191. \def\@beginPre{\global\setbox\@preConditionBox=%
  192.     \@beginMathIndentedPara{\hsize}{pre }}
  193. \def\@endPre{\@endMathIndentedPara}
  194. \newenvironment{postcond}{\@beginPost}{\@endPost}
  195. \def\post#1{\@beginPost#1\@endPost}
  196. \def\@beginPost{\global\setbox\@postConditionBox=%
  197.     \@beginMathIndentedPara{\hsize}{post }}
  198. \def\@endPost{\@endMathIndentedPara}
  199. \def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
  200.     \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
  201. \def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
  202. \def\@raggedRight{\rightskip=0pt plus 1fil \@setUpPenalties}
  203. \def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
  204.     {\@raggedRight\noindent$\relax}}
  205. \def\@endMathIndentedPara{\@endIndentedPara{\relax$}}
  206. \def\@setUpPenalties{\hyphenpenalty=-100 \linepenalty=200
  207.     \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}
  208. \def\@belowAndIndent#1#2{% place body in a separate box below and to the right
  209.     #1\hfil\break
  210.     \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
  211. \def\If#1\Then#2\Else#3\Fi{\vtop{%
  212.     \@beginMathIndentedPara{0pt}{if }#1\@endMathIndentedPara
  213.     \@beginMathIndentedPara{0pt}{then }#2\@endMathIndentedPara
  214.     \@beginMathIndentedPara{0pt}{else }#3\@endMathIndentedPara}}
  215. \def\SIf#1\Then#2\Else#3\Fi{\hbox to 0pt{\vtop{\@raggedRight\noindent$%
  216.     \kw{if }\nobreak#1\hskip 0.5em\penalty0
  217.     \kw{then }\nobreak#2\hskip 0.5em\penalty-100 % break here OK
  218.     \kw{else }\nobreak#3$}\hss}\hfil\break}
  219. \def\Let#1\In{\vtop{%
  220.     \@beginMathIndentedPara{0pt}{let }#1\hskip 0.5em
  221.     \kw{in}\@endMathIndentedPara}\hfil\break}
  222. \def\SLet#1\In#2{\hbox to 0pt{\vtop{\noindent$\kw{let }\nobreak#1\hskip 0.5em
  223.     \kw{in }\penalty-200 #2\relax$}\hss}\hfil\break}
  224. \newif\ifOtherwiseEncountered@
  225. \newtoks\@OtherwiseTokens
  226. \def\Cases#1{\hbox to 0pt\bgroup \vtop\bgroup
  227.         \@beginMathIndentedPara{\hsize}{cases }\strut
  228.             #1\hskip 0.5em\strut\kw{of}%
  229.         \@endMathIndentedPara
  230.         \bgroup % we might be in a nested case, so we have to
  231.         \OtherwiseEncountered@false \@changeLineSeparator 
  232.         \@beginCasesAlignment}
  233. \newtoks\@casesDef
  234. \def\leftCases{\@casesDef={$##$\hfil}}
  235. \def\rightCases{\@casesDef={\hfil$##$}}
  236. \rightCases
  237. \def\@beginCasesAlignment{\expandafter\halign\expandafter\bgroup
  238.     \the\@casesDef&$\,\rightarrow##$\hfil\cr}
  239. \def\Otherwise{\global\OtherwiseEncountered@true \global\@OtherwiseTokens=}
  240. \def\Endcases{\@endCasesAlignment \@setOtherwise \egroup \@setEndcases}
  241. \def\@endCasesAlignment{\crcr\egroup}
  242. \def\@setOtherwise{\ifOtherwiseEncountered@ % have an otherwise clause
  243.     \@beginMathIndentedPara{\hsize}{otherwise }%
  244.     \strut\the\@OtherwiseTokens\strut
  245.     \@endMathIndentedPara
  246.     \fi}
  247. \def\@setEndcases{\noindent
  248.     \strut\kw{end}\@ifnextchar [{\@unbracket}{\@finalCaseEnd}}
  249. \def\@unbracket[#1]{$#1$\@finalCaseEnd}
  250. \def\@finalCaseEnd{\egroup\hss\egroup\hfil\break}
  251. \def\DEF{\raise.5ex
  252.     \hbox{\footnotesize\underline{$\cal4$}}}% \cal4 is a \triangle
  253. \let\x=\times
  254. \def\Iff{\penalty-50\mskip 7mu plus 2mu minus 2mu
  255.     \Leftrightarrow\mskip 7mu plus 2mu minus 2mu}
  256. \let\iff=\Iff
  257. \def\Implies{\penalty-35\mskip 6mu plus 2mu minus 1mu \Rightarrow
  258.     \mskip 6mu plus 2mu minus 1mu}
  259. \let\implies=\Implies
  260. \let\And=\land
  261. \let\and=\And
  262. \let\Not=\neg
  263. \mathchardef\Exists="0239
  264. \mathchardef\Forall="0238
  265. \def\suchthat{\mathchar"2201 }
  266. \def\exists{\@ifstar{\@splitExists}{\@normalExists}}
  267. \def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
  268. \def\forall{\@ifstar{\@splitForall}{\@normalForall}}
  269. \def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
  270. \def\@normalExists#1#2{{\Exists#1}\suchthat #2}
  271. \def\@normalNExists#1#2{\hbox to 0pt{\raise0.15ex
  272.     \hbox{/}\hss}{\Exists#1}\suchthat #2}
  273. \def\@normalForall#1#2{{\Forall#1}\suchthat #2}
  274. \def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
  275. \def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
  276. \def\@splitNExists#1{\@belowAndIndent
  277.     {\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists#1\suchthat}}
  278. \def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
  279. \def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
  280. \def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}
  281. \let\compf=\circ
  282. \newenvironment{fn}{\parens@true\@beginVDMfunction}{\@endVDMfunction}
  283. \newenvironment{fn*}{\parens@false\@beginVDMfunction}{\@endVDMfunction}
  284. \newenvironment{vdmfn}{\@beginvdm\parens@true
  285.     \@beginVDMfunction}{\@endVDMfunction\@endvdm}
  286. \newenvironment{vdmfn*}{\@beginvdm\parens@false
  287.     \@beginVDMfunction}{\@endVDMfunction\@endvdm}
  288. \newbox\@fnNameBox
  289. \newif\ifsignatureEncountered@
  290. \newtoks\@signatureTokens
  291. \newbox\@fnDefnBox
  292. \newif\ifparens@
  293. \def\@beginVDMfunction#1#2{%
  294.     \setbox\@fnNameBox=\hbox{$#1$}%
  295.     \setbox\@preConditionBox=\box\voidb@x % for people who want to do
  296.     \setbox\@postConditionBox=\box\voidb@x% implicit defns
  297.     \@signatureTokens={}\signatureEncountered@false
  298.     \ifparens@
  299.         \@argumentListTokens={(#2)}
  300.     \else
  301.         \@argumentListTokens={#2}
  302.     \fi
  303.     \vskip\preFunctionSkip
  304.     \@beginVerticalVDM 
  305.     \bgroup
  306.     \advance\hsize by-\leftskip \leftskip=0pt % see \@beginVDMOperation
  307.     \preFunctionHook
  308.     \@beginFnDefn}
  309. \def\signature{\global\signatureEncountered@true \global\@signatureTokens=}
  310. \def\@beginFnDefn{\global\setbox\@fnDefnBox=\vtop\bgroup
  311.     \@raggedRight \hangindent=2em \hangafter=1
  312.     \noindent$\copy\@fnNameBox \the\@argumentListTokens 
  313.     \quad\DEF\quad\penalty-100 }
  314. \newskip\preFunctionSkip \preFunctionSkip=2ex plus .5ex minus .2ex
  315. \newskip\postFunctionSkip \postFunctionSkip=2ex plus .5ex minus .2ex
  316. \newskip\betweenSignatureAndBodySkip
  317. \betweenSignatureAndBodySkip=1.2ex plus .3ex minus .2ex
  318. \def\@endVDMfunction{%
  319.     $\egroup  % this ends the vtop we started in \@beginFnDefn
  320.     \ifsignatureEncountered@
  321.         \setbox0=\hbox{\unhbox\@fnNameBox$\;\mathpunct:\,$}%
  322.         \dimen255=\wd0 \noindent \box0
  323.         \vtop{\advance\hsize by-\dimen255 \@raggedRight
  324.             \noindent$\relax\the\@signatureTokens\relax$}%
  325.         \egroup % this matches the bgroup in \@beginVDMfunction
  326.         \vskip\betweenSignatureAndBodySkip
  327.         \betweenSignatureAndBodyHook
  328.     \else    \egroup % this matches the bgroup in \@beginVDMfunction
  329.     \fi
  330.     \moveright\VDMindent\box\@fnDefnBox
  331.     \vskip\postFunctionSkip
  332.     \ifvoid\@preConditionBox
  333.     \else \moveright\VDMindent\box\@preConditionBox
  334.           \vskip\postPreConditionSkip
  335.     \fi
  336.     \betweenPreAndPostConditionHook
  337.     \ifvoid\@postConditionBox
  338.     \else \moveright\VDMindent\box\@postConditionBox
  339.           \vskip\postOperationSkip
  340.     \fi
  341.     \postFunctionHook}
  342. \newcount\preFunctionPenalty \preFunctionPenalty=0
  343. \newcount\betweenSignatureAndBodyPenalty \betweenSignatureAndBodyPenalty=500
  344. \newcount\postFunctionPenalty \postFunctionPenalty=-500
  345. \def\preFunctionHook{\penalty\preFunctionPenalty }
  346. \def\betweenSignatureAndBodyHook{\penalty\betweenSignatureAndBodyPenalty }
  347. \def\postFunctionHook{\penalty\postFunctionPenalty }
  348. \def\to{\penalty-100\rightarrow}
  349. \def\LambdaFn{\@ifstar{\@splitLambdaFn}{\@normalLambdaFn}}
  350. \def\@normalLambdaFn#1#2{{\lambda#1}\suchthat#2}
  351. \def\@splitLambdaFn#1#2{% place body in a separate box below and to the right
  352.     {\lambda#1}\suchthat\hfil\break
  353.     \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
  354. \def\setof#1{\kw{set of }#1}
  355. \def\set#1{\{#1\}}
  356. \def\emptyset{\{\,\}}
  357. \let\inter=\cap \let\intersection=\inter
  358. \let\Inter=\bigcap \let\Intersection=\Inter
  359. \let\union=\cup
  360. \let\Union=\bigcup
  361. \mathchardef\minus="2200
  362. \def\diff{\minus} \let\difference=\diff
  363. \newMonadicOperator{\card}{card}
  364. \newMonadicOperator{\Min}{min}
  365. \newMonadicOperator{\Max}{max}
  366. \def\mapof#1#2{\kw{map }\nobreak#1\penalty-50\hskip .5em \kw{to }\nobreak#2}
  367. \def\mapinto#1#2{\kw{map }\nobreak#1\penalty-50
  368.     \hskip .5em \kw{into }\nobreak#2}
  369. \def\map#1{\{#1\}}
  370. \def\emptymap{\{\,\}}
  371. \def\owr{\dagger}
  372. \let\dres=\lhd
  373. \let\rres=\rhd % the right hand version
  374. \def\dsub{\hbox{$\rlap{$\lhd$}\minus$}}
  375. \def\rsub{\hbox{$\rlap{$\rhd$}\kern.23em\minus$}}
  376. \newMonadicOperator{\dom}{dom}
  377. \newMonadicOperator{\rng}{rng}
  378. \def\seqof#1{\kw{seq of }#1}
  379. \def\seq#1{[#1]}
  380. \def\emptyseq{[\,]}
  381. \newMonadicOperator{\len}{len}
  382. \newMonadicOperator{\hd}{hd}
  383. \newMonadicOperator{\tl}{tl}
  384. \newMonadicOperator{\elems}{elems}
  385. \newMonadicOperator{\inds}{inds}
  386. \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
  387.     \raise0.2ex\hbox{\it\char"12}}}}
  388. \def\type#1#2{{\vskip\preTypeSkip \@beginVerticalVDM
  389.     \advance\hsize by-\leftskip \leftskip=0pt % see \@beginVDMoperation
  390.     \moveright\VDMindent\vtop{\noindent$#1=#2$}
  391.     \vskip\postTypeSkip}}
  392. \newskip\preTypeSkip \preTypeSkip=1.2ex plus .5ex minus .3ex
  393. \newskip\postTypeSkip \postTypeSkip=1.2ex plus .5ex minus .3ex
  394. \newenvironment{composite}[1]{\@beginComposite{#1}}{\@endComposite}
  395. \newenvironment{composite*}[1]{\@beginSComposite{#1}}{\@endSComposite}
  396. \def\@beginSComposite#1{\vskip\preCompositeSkip
  397.     \noindent\hbox\bgroup
  398.     \kw{compose }$\relax#1\relax$\kw{ of }$\relax}
  399. \def\@endSComposite{\relax$\kw{ end}\egroup
  400.     \vskip\postCompositeSkip}
  401. \def\@beginComposite#1{\bgroup\vskip\preCompositeSkip
  402.     \@beginVerticalVDM
  403.     \advance\hsize by-\leftskip \leftskip=0pt % see \@beginVDMoperation
  404.     \moveright\VDMindent\vtop\bgroup
  405.     \noindent\kw{compose }$\relax#1\relax$\kw{ of}%\hfil\break
  406.     \@makeColonActive\@changeLineSeparator
  407.     \expandafter\halign\expandafter\bgroup\expandafter\qquad
  408.         \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  409. \def\@endComposite{\crcr\egroup % closes \halign
  410.     \kw{end}\egroup % ends the \vtop
  411.     \vskip\postCompositeSkip\egroup}
  412. \def\scompose#1#2{\@beginSComposite{#1}{#2}\@endSComposite}
  413. \newskip\preCompositeSkip \preCompositeSkip=1.2ex plus .5ex minus .3ex
  414. \newskip\postCompositeSkip \postCompositeSkip=1.2ex plus .5ex minus .3ex
  415. \newenvironment{record}{\@beginRecord}{\@endRecord}
  416. \def\@beginRecord#1{%
  417.     \vskip\preRecordSkip
  418.     \@beginVerticalVDM
  419.     \preRecordHook
  420.     \moveright\VDMindent\hbox\bgroup
  421.         \setbox0=\hbox{$#1$\enspace::\enspace}%
  422.         \@makeColonActive\@changeLineSeparator
  423.         \advance\hsize by-\wd0 \box0
  424.         \advance\hsize by-\leftskip
  425.             \leftskip=0pt % see \@beginVDMOperation
  426.         \vtop\bgroup\expandafter\halign\expandafter\bgroup
  427.             \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  428. \def\@endRecord{\crcr\egroup% closes halign
  429.     \egroup% closes vtop
  430.     \egroup% closes hbox
  431.     \vskip\postRecordSkip
  432.     \postRecordHook}
  433. \newtoks\@recordAlign
  434. \def\leftRecord{\@recordAlign={$##$\hfil}}
  435. \def\rightRecord{\@recordAlign={\hfil$##$}}
  436. \rightRecord
  437. \def\defrecord{\bgroup\@makeColonActive\@defrecord}
  438. \def\@defrecord#1#2{\@beginRecord{#1}#2\@endRecord\egroup}
  439. \newskip\preRecordSkip \preRecordSkip=.75ex plus .3ex minus .2ex
  440. \newskip\postRecordSkip \postRecordSkip=.75ex plus .3ex minus .2ex
  441. \newcount\preRecordPenalty \preRecordPenalty=0
  442. \newcount\postRecordPenalty \postRecordPenalty=-100
  443. \def\preRecordHook{\penalty\preRecordPenalty }
  444. \def\postRecordHook{\penalty\postRecordPenalty }
  445. \def\chg#1#2#3{\mu(#1,#2\mapsto#3)}
  446. \def\@mAth{\mathsurround=0pt} % p.353, \m@th
  447. \def\leftharpoonupfill{$\@mAth \mathord\leftharpoonup \mkern-6mu
  448.   \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
  449.   \mkern-6mu \mathord\minus$}  % p.357, \leftarrowfill
  450. \def\overleftharpoonup#1{{%
  451.   \boxmaxdepth=\maxdimen % this fixes Lamport's figures
  452.   \vbox{\ialign{##\crcr % p.359, \overleftarrow
  453.     \leftharpoonupfill\crcr\noalign{\kern-1pt \nointerlineskip}
  454.     $\hfil\displaystyle{#1}\hfil$\crcr}}}}
  455. \let\hook=\overleftharpoonup  % c'est simple comme bonjour
  456. \newenvironment{formula}{\@beginFormula}{\@endFormula}
  457. \def\form#1{\@beginFormula #1\@endFormula}
  458. \def\@beginFormula{\vskip\preFormulaSkip
  459.     \@beginVerticalVDM
  460.     \preFormulaHook
  461.     \bgroup
  462.     \advance\hsize by-\leftskip \leftskip=0pt % see \@beginVDMoperation
  463.     \moveright\VDMindent\vtop\bgroup\noindent$\displaystyle}
  464. \def\@endFormula{$\egroup % ends the vtop
  465.     \egroup % ends the overall group
  466.     \vskip\postFormulaSkip
  467.     \postFormulaHook}
  468. \newskip\preFormulaSkip \preFormulaSkip=1.2ex plus .5ex minus .3ex
  469. \newskip\postFormulaSkip \postFormulaSkip=1.2ex plus .5ex minus .3ex
  470. \newcount\preFormulaPenalty \preFormulaPenalty=0
  471. \newcount\postFormulaPenalty \postFormulaPenalty=-100
  472. \def\preFormulaHook{\penalty\preFormulaPenalty }
  473. \def\postFormulaHook{\penalty\postFormulaPenalty }
  474. \def\constantFont{\sc}
  475. \def\const#1{\hbox{\constantFont #1\/}}
  476. \def\T#1{\\\hbox to #1em{}}
  477. \newdimen\ProofIndent \ProofIndent=\VDMindent
  478. \newdimen\ProofNumberWidth \ProofNumberWidth=\parindent
  479. \newenvironment{proof}{\@beginProof}{\@endProof}
  480. \def\@beginProof{\vskip\preProofSkip
  481.     \preProofHook
  482.     \let\&=\@proofLine
  483.     \moveright\ProofIndent\vtop\bgroup
  484.         \advance\linewidth by-\ProofIndent
  485.         \begin{tabbing}%
  486.         \hbox to\ProofNumberWidth{}\=\kill}    % template line
  487. \def\@endProof{\end{tabbing}\advance\linewidth by\ProofIndent
  488.     \egroup % ends the \vtop
  489.     \vskip\postProofSkip
  490.     \postProofHook}
  491. \newskip\preProofSkip \preProofSkip=1.2ex plus .5ex minus .3ex
  492. \newskip\postProofSkip \postProofSkip=1.2ex plus .5ex minus .3ex
  493. \newcount\preProofPenalty \preProofPenalty=-100
  494. \newcount\postProofPenalty \postProofPenalty=0
  495. \def\preProofHook{\penalty\preProofPenalty }
  496. \def\postProofHook{\penalty\postProofPenalty }
  497.  
  498. \def\From{\@indentProof\kw{from }\=%
  499.     \global\advance\@indentLevel by 1
  500.     \@enterMathMode}
  501. \def\Infer{\global\advance\@indentLevel by-1
  502.     \@indentProof\kw{infer }\@enterMathMode}
  503. \def\@proofLine{\@indentProof\@enterMathMode}
  504. \def\by{\`}
  505. \newcount\@indentLevel \@indentLevel=1
  506. \newcount\@indentCount
  507. \def\@indentProof{% do \>, \@indentLevel times
  508.     \global\@indentCount=\@indentLevel
  509.     \@gloop \>\global\advance\@indentCount by-1
  510.     \ifnum\@indentCount>0
  511.     \repeat}
  512. \def\@gloop#1\repeat{\gdef\@body{#1}\@giterate}
  513. \def\@giterate{\@body \global\let\@gloopNext=\@giterate
  514.     \else \global\let\@gloopNext=\relax \fi \@gloopNext}
  515. \def\@enterMathMode{\def\@stopfield{$\egroup}$}
  516. \def\VDMauthor{M.Wolczko,
  517. CS Dept., Univ. of Manchester, UK. miw@uk.ac.man.cs.ux}
  518. \def\VDMversion{2.3}
  519. \@changeOtherMathcodes \@changeGlobalCatcodes
  520.